\begin{tabbing}
es{-}leaks(${\it es}$;$e$;$x$;${\it e'}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$a$:Atom1.\+
\\[0ex]$\neg$es{-}atom(${\it es}$;es{-}loc(${\it es}$; $e$);$a$)
\\[0ex]\& $\neg$es{-}state{-}when{-}without(${\it es}$;$e$;$x$):es{-}state{-}without(${\it es}$;es{-}loc(${\it es}$; $e$);$x$)$>>$$a$
\\[0ex]\& $\neg$es{-}rcv{-}atom(${\it es}$;$e$;$a$)
\\[0ex]\& \=es{-}isrcv(${\it es}$; ${\it e'}$)\+
\\[0ex]\& es{-}sender(${\it es}$; ${\it e'}$) $=$ $e$ $\in$ es{-}E(${\it es}$) \& es{-}val(${\it es}$; ${\it e'}$):es{-}valtype(${\it es}$; ${\it e'}$)$>>$$a$
\-\-
\end{tabbing}